es:ES, i:Id, P:(state@iProp).
@i stable state.P(state)  
 e@i. P(state after e)  (e':E. (e <loc e')  P((state when e'))) 

latex

Definitions	t  T, x:A. B(x), E, Type, loc(e), x:AB(x), Id, s = t, Prop, state after e, state@i, x:AB(x), f(a), x(s), (e <loc e'), P  Q, e@i. P(e), ES, x. t(x), @i stable state.P(state)  , <a,b>, pred(e), (state when e), P & Q, P  Q, b, Void, False, A, {T}, SQType(T), s ~ t, e  e' , P  Q, A/x,y. B(x;y), 1of(t), e'e.P(e'), P  Q
Lemmas	subtype rel self, es-le-pred, stable-implies2, es-pred wf, Id sq, es-loc-pred, state-after-pred, es-locl-iff, es-stable wf, es-state wf, event system wf, es-locl wf, es-state-after wf, Id wf, es-loc wf, es-E wf